Nuprl Lemma : mon_hom_p_comp 13,42

g, h:GrpSig{i}, k:GrpSig{k}, r:(|g||h|), s:(|h||k|).
IsMonHom{g,h}(r)  IsMonHom{h,k}(s)  IsMonHom{g,k}(s o r) 
latex


Upgroups 1
Definitions of StatementIsMonHom{M1,M2}(f)
Definitions, t  T, x f y, FunThru2op(A;B;opa;opb;f), P & Q, f o g, IsMonHom{M1,M2}(f), P  Q, x:A. B(x), P  Q, P  Q
Lemmasgrp sig wf, grp id wf, grp op wf, grp car wf

origin